$\forall$${\it ra}$, ${\it rt}$:(Id$\rightarrow$Id). Inj(Id;Id;${\it rt}$) $\Rightarrow$ Inj(Id;Id;${\it ra}$) $\Rightarrow$ Inj(Knd;Knd;$\lambda$$k$.kind{-}rename(${\it ra}$;${\it rt}$;$k$))